Nuprl Lemma : R-compat-sub
11,40
postcript
pdf
A
,
B
,
C
,
D
:Realizer.
A
C
B
D
{
C
||
D
A
||
B
}
latex
Definitions
{
T
}
Lemmas
R-compat
functionality
wrt
R-sub
origin
A, B, C, D:Realizer. A 
C 
B D {C || D A || B} A, B, C, D:Realizer. A C B D {C || D A || B}